[2016_hackcon] [REV] angry reverse

IDA Pro에서 hex ray error가 나와 다음과 같이 진행

400646: function frame is wrong

undefine(U) 이 후 Create Function(P)을 통해 함수 재 생성

from z3 import *

s = Solver()

a1 = []

for i in range(20):
    x = Int("x%d" % i)
    s.add(33<=x)
    s.add(x<=127)
    a1.append(x)

s.add(45471*a1[15] + 30501*a1[14] + 49830*a1[13] + 48077 * a1[10] + 27551 * a1[9] + 65182 * a1[8] + 11842 * a1[7] + 63310 * a1[6] + 13898 * a1[5] + 46609 * a1[3] + 28217 * a1[2] + -11000 * a1[0] - 46627 * a1[1] - 49550 * a1[4] - 49292 * a1[11] - 1629 * a1[12] - 9266 * a1[16] - 13808 * a1[17] - 30544 * a1[18] + 13392 * a1[19] == 19595924)
s.add(15715 * a1[16] + 41563 * a1[13] + 9679 * a1[11] + 42568 * a1[10] + 24678 * a1[9] + 60147 * a1[5] + 31059 * a1[4] + 62618 * a1[2] + -35420 * a1[0] + 24844 * a1[1] - 452 * a1[3] - 43245 * a1[6] - 42619 * a1[7] - 58888 * a1[8] - 8787 * a1[12] - 58185 * a1[14] - 23586 * a1[15] - 24464 * a1[17] - 16170 * a1[18] - 36313 * a1[19] == -7712995)
s.add(32456 * a1[18] + 7014 * a1[17] + 51654 * a1[16] + 55556 * a1[15] + 22609 * a1[10] + 54897 * a1[8] + 36361 * a1[5] + 1311 * a1[4] + 16505 * a1[3] + 11263 * a1[0] + 33126 * a1[1] - 7230 * a1[2] - 4486 * a1[6] - 4271 * a1[7] - 56477 * a1[9] - 53613 * a1[11] - 16104 * a1[12] - 61044 * a1[13] - 9955 * a1[14] + 38682 * a1[19] == 18417153)
s.add(53957 * a1[17] + 37569 * a1[16] + 37267 * a1[11] + 56559 * a1[8] + 7143 * a1[6] + 55131 * a1[5] + 56695 * a1[2] + 1453 * a1[0] + 5833 * a1[1] - 52080 * a1[3] - 12907 * a1[4] - 440 * a1[7] - 8768 * a1[9] - 10175 * a1[10] - 41500 * a1[12] - 38023 * a1[13] - 64810 * a1[14] - 47116 * a1[15] - 1231 * a1[18] - 35323 * a1[19] == 2411816)
s.add(532 * a1[18] + 54071 * a1[14] + 52009 * a1[10] + 21318 * a1[9] + 63357 * a1[8] + 36244 * a1[6] + 17077 * a1[4] + 11149 * a1[2] + 52001 * a1[0] + 23393 * a1[1] - 52350 * a1[3] - 3329 * a1[5] - 15462 * a1[7] - 63836 * a1[11] - 47848 * a1[12] - 7827 * a1[13] - 61128 * a1[15] - 6136 * a1[16] - 26085 * a1[17] + 18615 * a1[19]== 1410363)
s.add(29456 * a1[17] + 26894 * a1[16] + 2880 * a1[13] + 49930 * a1[12] + 37650 * a1[11] + 15331 * a1[6] + 43713 * a1[4] + 27438 * a1[2] + 61062 * a1[0] - 61196 * a1[1] - 53701 * a1[3] - 46647 * a1[5] - 40318 * a1[7] - 11339 * a1[8] - 30543 * a1[9] - 8872 * a1[10] - 19921 * a1[14] - 43687 * a1[15] - 17471 * a1[18] - 9958 * a1[19] == -5694468)
s.add( 12461 * a1[18] + 65022 * a1[17] + 47163 * a1[16] + 34096 * a1[4] + 15247 * a1[2] + 25773 * a1[0] + 11963 * a1[1] - 25741 * a1[3] - 49408 * a1[5] - 13033 * a1[6] - 21326 * a1[7] - 63232 * a1[8] - 3411 * a1[9] - 28620 * a1[10] - 12040 * a1[11] - 60222 * a1[12] - 46405 * a1[13] - 45780 * a1[14] - 38327 * a1[15] + 18881 * a1[19] == -11396530)
s.add(6326 * a1[16] + 28293 * a1[14] + 28675 * a1[11] + 12861 * a1[9] + 28372 * a1[4] + -9543 * a1[0] - 5154 * a1[1] - 54004 * a1[2] - 2642 * a1[3] - 46192 * a1[5] - 63583 * a1[6] - 33961 * a1[7] - 57733 * a1[8] - 46651 * a1[10] - 64514 * a1[12] - 33301 * a1[13] - 5465 * a1[15] - 26160 * a1[17] - 2122 * a1[18] + 33147 * a1[19] == -26341235)
s.add(23971 * a1[12] + 30329 * a1[10] + 34395 * a1[5] + 5517 * a1[3] + -28701 * a1[0] - 10703 * a1[1] - 27619 * a1[2] - 16331 * a1[4] - 8148 * a1[6] - 59420 * a1[7] - 42656 * a1[8] - 28243 * a1[9] - 18788 * a1[11] - 52430 * a1[13] - 52377 * a1[14] - 21498 * a1[15] - 2926 * a1[16] - 183 * a1[17] - 4660 * a1[18] + 49016 * a1[19] == -15360682)
s.add(10915 * a1[18] + 64416 * a1[17] + 51805 * a1[16] + 2544 * a1[14] + 22817 * a1[13] + 7099 * a1[12] + 63464 * a1[10] + 23276 * a1[9] + 53423 * a1[7] + 37222 * a1[6] + 32102 * a1[3] + 2612 * a1[2] + 62962 * a1[0] - 37744 * a1[1] - 36658 * a1[4] - 41772 * a1[5] - 16747 * a1[8] - 11898 * a1[11] - 55611 * a1[15] + 8479 * a1[19] == 24893817)
s.add(23945 * a1[18] + 9685 * a1[17] + 54267 * a1[16] + 1887 * a1[8] + 13573 * a1[4] + 31962 * a1[2] + 64729 * a1[0] + 4242 * a1[1] - 26135 * a1[3] - 28884 * a1[5] - 43353 * a1[6] - 22976 * a1[7] - 15302 * a1[9] - 33386 * a1[10] - 17807 * a1[11] - 27557 * a1[12] - 33154 * a1[13] - 53682 * a1[14] - 63448 * a1[15] - 31467 * a1[19] == -17431183)
s.add(46569 * a1[15] + 24947 * a1[14] + 22850 * a1[13] + 41728 * a1[12] + 1514 * a1[10] + 26166 * a1[9] + 49910 * a1[8] + 4730 * a1[6] + 11428 * a1[5] + 40496 * a1[2] + -32890 * a1[0] - 44062 * a1[1] - 29569 * a1[3] - 59223 * a1[4] - 33014 * a1[7] - 63540 * a1[11] - 21475 * a1[16] - 59868 * a1[17] - 63808 * a1[18] - 42006 * a1[19] == -19435013)
s.add(50245 * a1[17] + 25956 * a1[15] + 37474 * a1[12] + 59408 * a1[11] + 15266 * a1[10] + 1838 * a1[8] + 27458 * a1[7] + 14081 * a1[6] + 31108 * a1[0] - 5734 * a1[1] - 2969 * a1[2] - 38318 * a1[3] - 4302 * a1[4] - 5082 * a1[5] - 4607 * a1[9] - 42 * a1[13] - 54274 * a1[14] - 33513 * a1[16] - 36281 * a1[18] + 60905 * a1[19] == 19018520)
s.add(64158 * a1[18] + 31457 * a1[16] + 12412 * a1[14] + 11879 * a1[12] + 14242 * a1[11] + 5359 * a1[9] + 45380 * a1[2] + -26727 * a1[0] - 36498 * a1[1] - 25278 * a1[3] - 65469 * a1[4] - 63411 * a1[5] - 11827 * a1[6] - 33194 * a1[7] - 54207 * a1[8] - 47523 * a1[10] - 22348 * a1[13] - 17269 * a1[15] - 51301 * a1[17] - 39008 * a1[19] == -28544240)
s.add(42610 * a1[18] + 39139 * a1[16] + 37183 * a1[13] + 18068 * a1[11] + 36118 * a1[8] + 30807 * a1[7] + 11542 * a1[3] + 16698 * a1[0] + 9823 * a1[1] - 48029 * a1[2] - 57964 * a1[4] - 58848 * a1[5] - 43774 * a1[6] - 14155 * a1[9] - 15822 * a1[10] - 52308 * a1[12] - 38048 * a1[14] - 65437 * a1[15] - 29733 * a1[17] + 16964 * a1[19] == -11996652)
s.add(18750 * a1[18] + 61022 * a1[17] + 19853 * a1[16] + 14131 * a1[15] + 8163 * a1[13] + 56996 * a1[10] + 15502 * a1[7] + 22717 * a1[5] + 4683 * a1[4] + 56463 * a1[3] + 64704 * a1[2] + 17527 * a1[0] - 46323 * a1[1] - 63925 * a1[6] - 53380 * a1[8] - 65168 * a1[9] - 47740 * a1[11] - 26515 * a1[12] - 3864 * a1[14] + 2263 * a1[19] == 7830991)
s.add(21029 * a1[17] + 52828 * a1[14] + 46370 * a1[11] + 35647 * a1[10] + 64417 * a1[7] + 30063 * a1[4] + 15366 * a1[2] + -40635 * a1[0] + 58751 * a1[1] - 14997 * a1[3] - 27745 * a1[5] - 51122 * a1[6] - 15238 * a1[8] - 39488 * a1[9] - 47746 * a1[12] - 34066 * a1[13] - 45011 * a1[15] - 42181 * a1[16] - 34843 * a1[18] + 35777 * a1[19] == -694714)
s.add(7560 * a1[18] + 3710 * a1[16] + 46337 * a1[13] + 40308 * a1[11] + 20737 * a1[6] + 48502 * a1[5] + 25796 * a1[3] + 52737 * a1[2] + -10871 * a1[0] + 52804 * a1[1] - 42474 * a1[4] - 9473 * a1[7] - 55955 * a1[8] - 34929 * a1[9] - 58827 * a1[10] - 18550 * a1[12] - 17349 * a1[14] - 47215 * a1[15] - 52355 * a1[17] + 50743 * a1[19] == -4772683)
s.add(11292 * a1[18] + 22114 * a1[16] + 54053 * a1[12] + 19948 * a1[11] + 11 * a1[10] + 10039 * a1[9] + 19992 * a1[8] + 51167 * a1[7] + 39900 * a1[6] + 46510 * a1[5] + 55961 * a1[4] + 41846 * a1[2] + 7839 * a1[0] + 26505 * a1[1] - 3704 * a1[3] - 44936 * a1[13] - 23510 * a1[14] - 12555 * a1[15] - 60517 * a1[17] - 63711 * a1[19] == 14147533)
s.add(19059 * a1[16] + 5795 * a1[14] + 41600 * a1[13] + 1120 * a1[12] + 11816 * a1[11] + 38904 * a1[10] + 40862 * a1[8] + 8579 * a1[3] + -9187 * a1[0] + 905 * a1[1] - 9209 * a1[2] - 20023 * a1[4] - 26790 * a1[5] - 31881 * a1[6] - 53344 * a1[7] - 24334 * a1[9] - 49814 * a1[15] - 24931 * a1[17] - 16320 * a1[18] - 23459 * a1[19]== -14915502)

while s.check()==sat:
    print s.model()

'''
x11 = 89,
 x0 = 72,
 x9 = 86,
 x13 = 48,
 x16 = 103,
 x17 = 114,
 x8 = 86,
 x14 = 52,
 x2 = 67,
 x10 = 104,
 x1 = 65,
 x6 = 78,
 x18 = 89,
 x3 = 75,
 x12 = 83,
 x15 = 110,
 x19 = 125,
 x4 = 67,
 x5 = 79,
 x7 = 123
'''